COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	representations of functions: two approaches
C00003 00003	first approach: functions as association lists
C00006 00004	facts about alists
C00009 00005	second approach: functions as lists of numbers
C00013 ENDMK
C⊗;
;representations of functions: two approaches
(wipe-out)
(get-proofs nth prf ekl sys)
;first approach: functions as association lists

(proof appalist)

(decl dom (syntype: constant) (type: |GROUND→GROUND|))
(defax dom |∀xa y alist.dom nil=nil∧
                        dom((xa.y).alist)=xa.dom alist| )
(label domdef)

(decl range (syntype: constant) (type: |GROUND→GROUND|))
(defax range |∀xa y alist.range nil=nil∧
                          range((xa.y).alist)=y.range alist| )
(label rangedef)

(decl functp (syntype: constant) (type: |GROUND→TRUTHVAL|))
(define functp |∀alist.functp(alist)≡uniqueness dom(alist)|)
(label functdef)

(decl injectp (syntype: constant) (type: |GROUND→TRUTHVAL|))
(define injectp |∀alist.injectp(alist)≡functp(alist)∧uniqueness range(alist)|)
(label injectdef)

(decl (appalist) (syntype: constant) (type: |ground⊗ground→ground|))
(define appalist |∀alist y.appalist(y,alist)=cdr assoc(y,alist)|)
(label appalistdef)

(decl (samemap) (syntype: constant) (type: |ground⊗ground→truthval|))
(define samemap 
 |∀alist alist1.samemap(alist,alist1)≡
                mklset dom(alist)=mklset dom(alist1)∧
                (∀y.yεmklset dom(alist)⊃appalist(y,alist)=appalist(y,alist1))|)
(label samemapdef)

(decl permutp (syntype: constant) (type: |GROUND→TRUTHVAL|))
(define permutp |∀alist.permutp(alist)≡
                        functp(alist)∧mklset(dom(alist))=mklset(range(alist))|)
(label permutp_def)

(axiom |∀chi.chi(nil)∧(∀xa y alist.chi(alist)⊃chi((xa.y).alist))⊃(∀alist.chi(alist))|)
(label alistinduction)

;facts about alists

(proof alistfacts)

(axiom |∀alist.listp(dom alist)|)
(label domsort)(label simpinfo)

(axiom |∀alist.listp(range alist)|)
(label rangesort)(label simpinfo)

(axiom |∀alist.length (dom(alist))=length alist|)
(label domlength)

(axiom |∀alist.length(dom(alist))=length(range(alist))|)
(label domrangelength)

(axiom |∀alist y.sexp appalist(y,alist)|)
(label appalistsort)(label simpinfo)

(axiom |∀alist y.¬yεmklset(dom(alist))⊃appalist(y,alist)=nil|)
(label trivial_appalist)

;Exercise:
;∀alist z.member(z,range alist)⊃(∃x.member(x.z,alist))
;(label member_range)

;∀alist x z.member(x.z,alist)⊃member(z,range(alist))
;(label membership_alist_range)

;∀alist x z.x=appalist(z,alist)∧atom assoc(z,alist)⊃null x
;(label trivial_assoc)

(axiom |∀alist.samemap(alist,alist)|)
(label samemap_equivalence)

(axiom |∀alist alist1.samemap(alist,alist1)⊃samemap(alist1,alist)|)
(label samemap_equivalence)

(axiom 
   |∀alist alist1 alist2.
       samemap(alist,alist1)∧samemap(alist1,alist2)⊃samemap(alist,alist2)|)
(label samemap_equivalence)

(axiom |∀alist1 alist2.samemap(alist1,alist2)≡
                       (mklset(dom(alist1))=mklset(dom(alist2))∧
                       (∀x.appalist(x,alist1)=appalist(x,alist2)))|)
(label samemap_def1)
;second approach: functions as lists of numbers

(proof appl)

(decl appl (syntype: constant) (type: |ground⊗ground→ground|))
(define appl |∀u i.appl(u,i)=nth(u,i)|)
(label appldef)

;extensionality for functions 

(axiom |∀u v.length u=length v∧(∀i.i<length u⊃appl(u,i)=appl(v,i))⊃u=v|)
(label extensionality)
 
(axiom |∀u i.i<length u ⊃ sexp(appl(u,i))∧member(appl(u,i),u)|)
(label applfacts) (label simpinfo)

;predicates for functions 

(decl (into) (syntype: constant) (type: |ground→truthval|))
(define into |∀u.into(u)=(∀n.n<length u⊃natnum nth(u,n)∧nth(u,n)<length u)|)
(label intodef)

(decl (onto) (syntype: constant) (type: |ground→truthval|))
(define onto |∀u.onto(u)=(into(u)∧(∀n.n<length u⊃member(n,u)))|)
(label ontodef)
 
(decl (perm) (syntype: constant) (type: |ground→truthval|))
(define perm |∀u.perm(u)=onto(u)|)

;injectivity is given by the predicate inj

(save-proofs appl)